0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 187 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 329 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 21 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 0 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 PiDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 PiDP
↳17 PiDPToQDPProof (⇒, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
↳21 PiDP
↳22 UsableRulesProof (⇔, 0 ms)
↳23 PiDP
↳24 PiDPToQDPProof (⇒, 0 ms)
↳25 QDP
↳26 QDPSizeChangeProof (⇔, 0 ms)
↳27 YES
↳28 PiDP
↳29 UsableRulesProof (⇔, 0 ms)
↳30 PiDP
↳31 PiDPToQDPProof (⇒, 0 ms)
↳32 QDP
↳33 UsableRulesReductionPairsProof (⇔, 119 ms)
↳34 QDP
↳35 PisEmptyProof (⇔, 0 ms)
↳36 YES
CONVERTC_IN_GGA(.(0, .(0, X1)), X2, X3) → U13_GGA(X1, X2, X3, convertA_in_gga(X1, X2, X4))
CONVERTC_IN_GGA(.(0, .(0, X1)), X2, X3) → CONVERTA_IN_GGA(X1, X2, X4)
CONVERTA_IN_GGA(.(0, X1), X2, X3) → U1_GGA(X1, X2, X3, convertA_in_gga(X1, X2, X4))
CONVERTA_IN_GGA(.(0, X1), X2, X3) → CONVERTA_IN_GGA(X1, X2, X4)
CONVERTA_IN_GGA(.(0, X1), X2, X3) → U2_GGA(X1, X2, X3, convertcA_in_gga(X1, X2, X4))
U2_GGA(X1, X2, X3, convertcA_out_gga(X1, X2, X4)) → U3_GGA(X1, X2, X3, timesB_in_gga(X4, X2, X3))
U2_GGA(X1, X2, X3, convertcA_out_gga(X1, X2, X4)) → TIMESB_IN_GGA(X4, X2, X3)
TIMESB_IN_GGA(s(X1), X2, X3) → U5_GGA(X1, X2, X3, timesB_in_gga(X1, X2, X4))
TIMESB_IN_GGA(s(X1), X2, X3) → TIMESB_IN_GGA(X1, X2, X4)
TIMESB_IN_GGA(s(X1), X2, X3) → U6_GGA(X1, X2, X3, timescB_in_gga(X1, X2, X4))
U6_GGA(X1, X2, X3, timescB_out_gga(X1, X2, X4)) → U7_GGA(X1, X2, X3, plusD_in_gga(X2, X4, X3))
U6_GGA(X1, X2, X3, timescB_out_gga(X1, X2, X4)) → PLUSD_IN_GGA(X2, X4, X3)
PLUSD_IN_GGA(s(X1), X2, s(X3)) → U8_GGA(X1, X2, X3, plusD_in_gga(X1, X2, X3))
PLUSD_IN_GGA(s(X1), X2, s(X3)) → PLUSD_IN_GGA(X1, X2, X3)
CONVERTA_IN_GGA(.(s(X1), X2), X3, s(X4)) → U4_GGA(X1, X2, X3, X4, convertC_in_gga(.(X1, X2), X3, X4))
CONVERTA_IN_GGA(.(s(X1), X2), X3, s(X4)) → CONVERTC_IN_GGA(.(X1, X2), X3, X4)
CONVERTC_IN_GGA(.(0, .(0, X1)), X2, X3) → U14_GGA(X1, X2, X3, convertcA_in_gga(X1, X2, X4))
U14_GGA(X1, X2, X3, convertcA_out_gga(X1, X2, X4)) → U15_GGA(X1, X2, X3, timesB_in_gga(X4, X2, X5))
U14_GGA(X1, X2, X3, convertcA_out_gga(X1, X2, X4)) → TIMESB_IN_GGA(X4, X2, X5)
U14_GGA(X1, X2, X3, convertcA_out_gga(X1, X2, X4)) → U16_GGA(X1, X2, X3, timescB_in_gga(X4, X2, X5))
U16_GGA(X1, X2, X3, timescB_out_gga(X4, X2, X5)) → U17_GGA(X1, X2, X3, timesE_in_gga(X5, X2, X3))
U16_GGA(X1, X2, X3, timescB_out_gga(X4, X2, X5)) → TIMESE_IN_GGA(X5, X2, X3)
TIMESE_IN_GGA(s(X1), X2, X3) → U10_GGA(X1, X2, X3, timesB_in_gga(X1, X2, X4))
TIMESE_IN_GGA(s(X1), X2, X3) → TIMESB_IN_GGA(X1, X2, X4)
TIMESE_IN_GGA(s(X1), X2, X3) → U11_GGA(X1, X2, X3, timescB_in_gga(X1, X2, X4))
U11_GGA(X1, X2, X3, timescB_out_gga(X1, X2, X4)) → U12_GGA(X1, X2, X3, plusF_in_gga(X2, X4, X3))
U11_GGA(X1, X2, X3, timescB_out_gga(X1, X2, X4)) → PLUSF_IN_GGA(X2, X4, X3)
PLUSF_IN_GGA(s(X1), X2, s(X3)) → U9_GGA(X1, X2, X3, plusF_in_gga(X1, X2, X3))
PLUSF_IN_GGA(s(X1), X2, s(X3)) → PLUSF_IN_GGA(X1, X2, X3)
CONVERTC_IN_GGA(.(0, .(s(X1), X2)), X3, X4) → U18_GGA(X1, X2, X3, X4, convertC_in_gga(.(X1, X2), X3, X5))
CONVERTC_IN_GGA(.(0, .(s(X1), X2)), X3, X4) → CONVERTC_IN_GGA(.(X1, X2), X3, X5)
CONVERTC_IN_GGA(.(0, .(s(X1), X2)), X3, X4) → U19_GGA(X1, X2, X3, X4, convertcC_in_gga(.(X1, X2), X3, X5))
U19_GGA(X1, X2, X3, X4, convertcC_out_gga(.(X1, X2), X3, X5)) → U20_GGA(X1, X2, X3, X4, timesE_in_gga(s(X5), X3, X4))
U19_GGA(X1, X2, X3, X4, convertcC_out_gga(.(X1, X2), X3, X5)) → TIMESE_IN_GGA(s(X5), X3, X4)
CONVERTC_IN_GGA(.(s(0), X1), X2, s(X3)) → U21_GGA(X1, X2, X3, convertA_in_gga(X1, X2, X4))
CONVERTC_IN_GGA(.(s(0), X1), X2, s(X3)) → CONVERTA_IN_GGA(X1, X2, X4)
CONVERTC_IN_GGA(.(s(0), X1), X2, s(X3)) → U22_GGA(X1, X2, X3, convertcA_in_gga(X1, X2, X4))
U22_GGA(X1, X2, X3, convertcA_out_gga(X1, X2, X4)) → U23_GGA(X1, X2, X3, timesE_in_gga(X4, X2, X3))
U22_GGA(X1, X2, X3, convertcA_out_gga(X1, X2, X4)) → TIMESE_IN_GGA(X4, X2, X3)
CONVERTC_IN_GGA(.(s(s(X1)), X2), X3, s(s(X4))) → U24_GGA(X1, X2, X3, X4, convertC_in_gga(.(X1, X2), X3, X4))
CONVERTC_IN_GGA(.(s(s(X1)), X2), X3, s(s(X4))) → CONVERTC_IN_GGA(.(X1, X2), X3, X4)
convertcA_in_gga([], X1, 0) → convertcA_out_gga([], X1, 0)
convertcA_in_gga(.(0, X1), X2, X3) → U26_gga(X1, X2, X3, convertcA_in_gga(X1, X2, X4))
convertcA_in_gga(.(s(X1), X2), X3, s(X4)) → U28_gga(X1, X2, X3, X4, convertcC_in_gga(.(X1, X2), X3, X4))
convertcC_in_gga([], X1, 0) → convertcC_out_gga([], X1, 0)
convertcC_in_gga(.(0, []), X1, 0) → convertcC_out_gga(.(0, []), X1, 0)
convertcC_in_gga(.(0, .(0, X1)), X2, X3) → U32_gga(X1, X2, X3, convertcA_in_gga(X1, X2, X4))
U32_gga(X1, X2, X3, convertcA_out_gga(X1, X2, X4)) → U33_gga(X1, X2, X3, timescB_in_gga(X4, X2, X5))
timescB_in_gga(0, X1, 0) → timescB_out_gga(0, X1, 0)
timescB_in_gga(s(X1), X2, X3) → U29_gga(X1, X2, X3, timescB_in_gga(X1, X2, X4))
U29_gga(X1, X2, X3, timescB_out_gga(X1, X2, X4)) → U30_gga(X1, X2, X3, pluscD_in_gga(X2, X4, X3))
pluscD_in_gga(0, X1, X1) → pluscD_out_gga(0, X1, X1)
pluscD_in_gga(s(X1), X2, s(X3)) → U31_gga(X1, X2, X3, pluscD_in_gga(X1, X2, X3))
U31_gga(X1, X2, X3, pluscD_out_gga(X1, X2, X3)) → pluscD_out_gga(s(X1), X2, s(X3))
U30_gga(X1, X2, X3, pluscD_out_gga(X2, X4, X3)) → timescB_out_gga(s(X1), X2, X3)
U33_gga(X1, X2, X3, timescB_out_gga(X4, X2, X5)) → U34_gga(X1, X2, X3, timescE_in_gga(X5, X2, X3))
timescE_in_gga(0, X1, 0) → timescE_out_gga(0, X1, 0)
timescE_in_gga(s(X1), X2, X3) → U41_gga(X1, X2, X3, timescB_in_gga(X1, X2, X4))
U41_gga(X1, X2, X3, timescB_out_gga(X1, X2, X4)) → U42_gga(X1, X2, X3, pluscF_in_gga(X2, X4, X3))
pluscF_in_gga(0, X1, X1) → pluscF_out_gga(0, X1, X1)
pluscF_in_gga(s(X1), X2, s(X3)) → U40_gga(X1, X2, X3, pluscF_in_gga(X1, X2, X3))
U40_gga(X1, X2, X3, pluscF_out_gga(X1, X2, X3)) → pluscF_out_gga(s(X1), X2, s(X3))
U42_gga(X1, X2, X3, pluscF_out_gga(X2, X4, X3)) → timescE_out_gga(s(X1), X2, X3)
U34_gga(X1, X2, X3, timescE_out_gga(X5, X2, X3)) → convertcC_out_gga(.(0, .(0, X1)), X2, X3)
convertcC_in_gga(.(0, .(s(X1), X2)), X3, X4) → U35_gga(X1, X2, X3, X4, convertcC_in_gga(.(X1, X2), X3, X5))
convertcC_in_gga(.(s(0), X1), X2, s(X3)) → U37_gga(X1, X2, X3, convertcA_in_gga(X1, X2, X4))
U37_gga(X1, X2, X3, convertcA_out_gga(X1, X2, X4)) → U38_gga(X1, X2, X3, timescE_in_gga(X4, X2, X3))
U38_gga(X1, X2, X3, timescE_out_gga(X4, X2, X3)) → convertcC_out_gga(.(s(0), X1), X2, s(X3))
convertcC_in_gga(.(s(s(X1)), X2), X3, s(s(X4))) → U39_gga(X1, X2, X3, X4, convertcC_in_gga(.(X1, X2), X3, X4))
U39_gga(X1, X2, X3, X4, convertcC_out_gga(.(X1, X2), X3, X4)) → convertcC_out_gga(.(s(s(X1)), X2), X3, s(s(X4)))
U35_gga(X1, X2, X3, X4, convertcC_out_gga(.(X1, X2), X3, X5)) → U36_gga(X1, X2, X3, X4, timescE_in_gga(s(X5), X3, X4))
U36_gga(X1, X2, X3, X4, timescE_out_gga(s(X5), X3, X4)) → convertcC_out_gga(.(0, .(s(X1), X2)), X3, X4)
U28_gga(X1, X2, X3, X4, convertcC_out_gga(.(X1, X2), X3, X4)) → convertcA_out_gga(.(s(X1), X2), X3, s(X4))
U26_gga(X1, X2, X3, convertcA_out_gga(X1, X2, X4)) → U27_gga(X1, X2, X3, timescB_in_gga(X4, X2, X3))
U27_gga(X1, X2, X3, timescB_out_gga(X4, X2, X3)) → convertcA_out_gga(.(0, X1), X2, X3)
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
CONVERTC_IN_GGA(.(0, .(0, X1)), X2, X3) → U13_GGA(X1, X2, X3, convertA_in_gga(X1, X2, X4))
CONVERTC_IN_GGA(.(0, .(0, X1)), X2, X3) → CONVERTA_IN_GGA(X1, X2, X4)
CONVERTA_IN_GGA(.(0, X1), X2, X3) → U1_GGA(X1, X2, X3, convertA_in_gga(X1, X2, X4))
CONVERTA_IN_GGA(.(0, X1), X2, X3) → CONVERTA_IN_GGA(X1, X2, X4)
CONVERTA_IN_GGA(.(0, X1), X2, X3) → U2_GGA(X1, X2, X3, convertcA_in_gga(X1, X2, X4))
U2_GGA(X1, X2, X3, convertcA_out_gga(X1, X2, X4)) → U3_GGA(X1, X2, X3, timesB_in_gga(X4, X2, X3))
U2_GGA(X1, X2, X3, convertcA_out_gga(X1, X2, X4)) → TIMESB_IN_GGA(X4, X2, X3)
TIMESB_IN_GGA(s(X1), X2, X3) → U5_GGA(X1, X2, X3, timesB_in_gga(X1, X2, X4))
TIMESB_IN_GGA(s(X1), X2, X3) → TIMESB_IN_GGA(X1, X2, X4)
TIMESB_IN_GGA(s(X1), X2, X3) → U6_GGA(X1, X2, X3, timescB_in_gga(X1, X2, X4))
U6_GGA(X1, X2, X3, timescB_out_gga(X1, X2, X4)) → U7_GGA(X1, X2, X3, plusD_in_gga(X2, X4, X3))
U6_GGA(X1, X2, X3, timescB_out_gga(X1, X2, X4)) → PLUSD_IN_GGA(X2, X4, X3)
PLUSD_IN_GGA(s(X1), X2, s(X3)) → U8_GGA(X1, X2, X3, plusD_in_gga(X1, X2, X3))
PLUSD_IN_GGA(s(X1), X2, s(X3)) → PLUSD_IN_GGA(X1, X2, X3)
CONVERTA_IN_GGA(.(s(X1), X2), X3, s(X4)) → U4_GGA(X1, X2, X3, X4, convertC_in_gga(.(X1, X2), X3, X4))
CONVERTA_IN_GGA(.(s(X1), X2), X3, s(X4)) → CONVERTC_IN_GGA(.(X1, X2), X3, X4)
CONVERTC_IN_GGA(.(0, .(0, X1)), X2, X3) → U14_GGA(X1, X2, X3, convertcA_in_gga(X1, X2, X4))
U14_GGA(X1, X2, X3, convertcA_out_gga(X1, X2, X4)) → U15_GGA(X1, X2, X3, timesB_in_gga(X4, X2, X5))
U14_GGA(X1, X2, X3, convertcA_out_gga(X1, X2, X4)) → TIMESB_IN_GGA(X4, X2, X5)
U14_GGA(X1, X2, X3, convertcA_out_gga(X1, X2, X4)) → U16_GGA(X1, X2, X3, timescB_in_gga(X4, X2, X5))
U16_GGA(X1, X2, X3, timescB_out_gga(X4, X2, X5)) → U17_GGA(X1, X2, X3, timesE_in_gga(X5, X2, X3))
U16_GGA(X1, X2, X3, timescB_out_gga(X4, X2, X5)) → TIMESE_IN_GGA(X5, X2, X3)
TIMESE_IN_GGA(s(X1), X2, X3) → U10_GGA(X1, X2, X3, timesB_in_gga(X1, X2, X4))
TIMESE_IN_GGA(s(X1), X2, X3) → TIMESB_IN_GGA(X1, X2, X4)
TIMESE_IN_GGA(s(X1), X2, X3) → U11_GGA(X1, X2, X3, timescB_in_gga(X1, X2, X4))
U11_GGA(X1, X2, X3, timescB_out_gga(X1, X2, X4)) → U12_GGA(X1, X2, X3, plusF_in_gga(X2, X4, X3))
U11_GGA(X1, X2, X3, timescB_out_gga(X1, X2, X4)) → PLUSF_IN_GGA(X2, X4, X3)
PLUSF_IN_GGA(s(X1), X2, s(X3)) → U9_GGA(X1, X2, X3, plusF_in_gga(X1, X2, X3))
PLUSF_IN_GGA(s(X1), X2, s(X3)) → PLUSF_IN_GGA(X1, X2, X3)
CONVERTC_IN_GGA(.(0, .(s(X1), X2)), X3, X4) → U18_GGA(X1, X2, X3, X4, convertC_in_gga(.(X1, X2), X3, X5))
CONVERTC_IN_GGA(.(0, .(s(X1), X2)), X3, X4) → CONVERTC_IN_GGA(.(X1, X2), X3, X5)
CONVERTC_IN_GGA(.(0, .(s(X1), X2)), X3, X4) → U19_GGA(X1, X2, X3, X4, convertcC_in_gga(.(X1, X2), X3, X5))
U19_GGA(X1, X2, X3, X4, convertcC_out_gga(.(X1, X2), X3, X5)) → U20_GGA(X1, X2, X3, X4, timesE_in_gga(s(X5), X3, X4))
U19_GGA(X1, X2, X3, X4, convertcC_out_gga(.(X1, X2), X3, X5)) → TIMESE_IN_GGA(s(X5), X3, X4)
CONVERTC_IN_GGA(.(s(0), X1), X2, s(X3)) → U21_GGA(X1, X2, X3, convertA_in_gga(X1, X2, X4))
CONVERTC_IN_GGA(.(s(0), X1), X2, s(X3)) → CONVERTA_IN_GGA(X1, X2, X4)
CONVERTC_IN_GGA(.(s(0), X1), X2, s(X3)) → U22_GGA(X1, X2, X3, convertcA_in_gga(X1, X2, X4))
U22_GGA(X1, X2, X3, convertcA_out_gga(X1, X2, X4)) → U23_GGA(X1, X2, X3, timesE_in_gga(X4, X2, X3))
U22_GGA(X1, X2, X3, convertcA_out_gga(X1, X2, X4)) → TIMESE_IN_GGA(X4, X2, X3)
CONVERTC_IN_GGA(.(s(s(X1)), X2), X3, s(s(X4))) → U24_GGA(X1, X2, X3, X4, convertC_in_gga(.(X1, X2), X3, X4))
CONVERTC_IN_GGA(.(s(s(X1)), X2), X3, s(s(X4))) → CONVERTC_IN_GGA(.(X1, X2), X3, X4)
convertcA_in_gga([], X1, 0) → convertcA_out_gga([], X1, 0)
convertcA_in_gga(.(0, X1), X2, X3) → U26_gga(X1, X2, X3, convertcA_in_gga(X1, X2, X4))
convertcA_in_gga(.(s(X1), X2), X3, s(X4)) → U28_gga(X1, X2, X3, X4, convertcC_in_gga(.(X1, X2), X3, X4))
convertcC_in_gga([], X1, 0) → convertcC_out_gga([], X1, 0)
convertcC_in_gga(.(0, []), X1, 0) → convertcC_out_gga(.(0, []), X1, 0)
convertcC_in_gga(.(0, .(0, X1)), X2, X3) → U32_gga(X1, X2, X3, convertcA_in_gga(X1, X2, X4))
U32_gga(X1, X2, X3, convertcA_out_gga(X1, X2, X4)) → U33_gga(X1, X2, X3, timescB_in_gga(X4, X2, X5))
timescB_in_gga(0, X1, 0) → timescB_out_gga(0, X1, 0)
timescB_in_gga(s(X1), X2, X3) → U29_gga(X1, X2, X3, timescB_in_gga(X1, X2, X4))
U29_gga(X1, X2, X3, timescB_out_gga(X1, X2, X4)) → U30_gga(X1, X2, X3, pluscD_in_gga(X2, X4, X3))
pluscD_in_gga(0, X1, X1) → pluscD_out_gga(0, X1, X1)
pluscD_in_gga(s(X1), X2, s(X3)) → U31_gga(X1, X2, X3, pluscD_in_gga(X1, X2, X3))
U31_gga(X1, X2, X3, pluscD_out_gga(X1, X2, X3)) → pluscD_out_gga(s(X1), X2, s(X3))
U30_gga(X1, X2, X3, pluscD_out_gga(X2, X4, X3)) → timescB_out_gga(s(X1), X2, X3)
U33_gga(X1, X2, X3, timescB_out_gga(X4, X2, X5)) → U34_gga(X1, X2, X3, timescE_in_gga(X5, X2, X3))
timescE_in_gga(0, X1, 0) → timescE_out_gga(0, X1, 0)
timescE_in_gga(s(X1), X2, X3) → U41_gga(X1, X2, X3, timescB_in_gga(X1, X2, X4))
U41_gga(X1, X2, X3, timescB_out_gga(X1, X2, X4)) → U42_gga(X1, X2, X3, pluscF_in_gga(X2, X4, X3))
pluscF_in_gga(0, X1, X1) → pluscF_out_gga(0, X1, X1)
pluscF_in_gga(s(X1), X2, s(X3)) → U40_gga(X1, X2, X3, pluscF_in_gga(X1, X2, X3))
U40_gga(X1, X2, X3, pluscF_out_gga(X1, X2, X3)) → pluscF_out_gga(s(X1), X2, s(X3))
U42_gga(X1, X2, X3, pluscF_out_gga(X2, X4, X3)) → timescE_out_gga(s(X1), X2, X3)
U34_gga(X1, X2, X3, timescE_out_gga(X5, X2, X3)) → convertcC_out_gga(.(0, .(0, X1)), X2, X3)
convertcC_in_gga(.(0, .(s(X1), X2)), X3, X4) → U35_gga(X1, X2, X3, X4, convertcC_in_gga(.(X1, X2), X3, X5))
convertcC_in_gga(.(s(0), X1), X2, s(X3)) → U37_gga(X1, X2, X3, convertcA_in_gga(X1, X2, X4))
U37_gga(X1, X2, X3, convertcA_out_gga(X1, X2, X4)) → U38_gga(X1, X2, X3, timescE_in_gga(X4, X2, X3))
U38_gga(X1, X2, X3, timescE_out_gga(X4, X2, X3)) → convertcC_out_gga(.(s(0), X1), X2, s(X3))
convertcC_in_gga(.(s(s(X1)), X2), X3, s(s(X4))) → U39_gga(X1, X2, X3, X4, convertcC_in_gga(.(X1, X2), X3, X4))
U39_gga(X1, X2, X3, X4, convertcC_out_gga(.(X1, X2), X3, X4)) → convertcC_out_gga(.(s(s(X1)), X2), X3, s(s(X4)))
U35_gga(X1, X2, X3, X4, convertcC_out_gga(.(X1, X2), X3, X5)) → U36_gga(X1, X2, X3, X4, timescE_in_gga(s(X5), X3, X4))
U36_gga(X1, X2, X3, X4, timescE_out_gga(s(X5), X3, X4)) → convertcC_out_gga(.(0, .(s(X1), X2)), X3, X4)
U28_gga(X1, X2, X3, X4, convertcC_out_gga(.(X1, X2), X3, X4)) → convertcA_out_gga(.(s(X1), X2), X3, s(X4))
U26_gga(X1, X2, X3, convertcA_out_gga(X1, X2, X4)) → U27_gga(X1, X2, X3, timescB_in_gga(X4, X2, X3))
U27_gga(X1, X2, X3, timescB_out_gga(X4, X2, X3)) → convertcA_out_gga(.(0, X1), X2, X3)
PLUSF_IN_GGA(s(X1), X2, s(X3)) → PLUSF_IN_GGA(X1, X2, X3)
convertcA_in_gga([], X1, 0) → convertcA_out_gga([], X1, 0)
convertcA_in_gga(.(0, X1), X2, X3) → U26_gga(X1, X2, X3, convertcA_in_gga(X1, X2, X4))
convertcA_in_gga(.(s(X1), X2), X3, s(X4)) → U28_gga(X1, X2, X3, X4, convertcC_in_gga(.(X1, X2), X3, X4))
convertcC_in_gga([], X1, 0) → convertcC_out_gga([], X1, 0)
convertcC_in_gga(.(0, []), X1, 0) → convertcC_out_gga(.(0, []), X1, 0)
convertcC_in_gga(.(0, .(0, X1)), X2, X3) → U32_gga(X1, X2, X3, convertcA_in_gga(X1, X2, X4))
U32_gga(X1, X2, X3, convertcA_out_gga(X1, X2, X4)) → U33_gga(X1, X2, X3, timescB_in_gga(X4, X2, X5))
timescB_in_gga(0, X1, 0) → timescB_out_gga(0, X1, 0)
timescB_in_gga(s(X1), X2, X3) → U29_gga(X1, X2, X3, timescB_in_gga(X1, X2, X4))
U29_gga(X1, X2, X3, timescB_out_gga(X1, X2, X4)) → U30_gga(X1, X2, X3, pluscD_in_gga(X2, X4, X3))
pluscD_in_gga(0, X1, X1) → pluscD_out_gga(0, X1, X1)
pluscD_in_gga(s(X1), X2, s(X3)) → U31_gga(X1, X2, X3, pluscD_in_gga(X1, X2, X3))
U31_gga(X1, X2, X3, pluscD_out_gga(X1, X2, X3)) → pluscD_out_gga(s(X1), X2, s(X3))
U30_gga(X1, X2, X3, pluscD_out_gga(X2, X4, X3)) → timescB_out_gga(s(X1), X2, X3)
U33_gga(X1, X2, X3, timescB_out_gga(X4, X2, X5)) → U34_gga(X1, X2, X3, timescE_in_gga(X5, X2, X3))
timescE_in_gga(0, X1, 0) → timescE_out_gga(0, X1, 0)
timescE_in_gga(s(X1), X2, X3) → U41_gga(X1, X2, X3, timescB_in_gga(X1, X2, X4))
U41_gga(X1, X2, X3, timescB_out_gga(X1, X2, X4)) → U42_gga(X1, X2, X3, pluscF_in_gga(X2, X4, X3))
pluscF_in_gga(0, X1, X1) → pluscF_out_gga(0, X1, X1)
pluscF_in_gga(s(X1), X2, s(X3)) → U40_gga(X1, X2, X3, pluscF_in_gga(X1, X2, X3))
U40_gga(X1, X2, X3, pluscF_out_gga(X1, X2, X3)) → pluscF_out_gga(s(X1), X2, s(X3))
U42_gga(X1, X2, X3, pluscF_out_gga(X2, X4, X3)) → timescE_out_gga(s(X1), X2, X3)
U34_gga(X1, X2, X3, timescE_out_gga(X5, X2, X3)) → convertcC_out_gga(.(0, .(0, X1)), X2, X3)
convertcC_in_gga(.(0, .(s(X1), X2)), X3, X4) → U35_gga(X1, X2, X3, X4, convertcC_in_gga(.(X1, X2), X3, X5))
convertcC_in_gga(.(s(0), X1), X2, s(X3)) → U37_gga(X1, X2, X3, convertcA_in_gga(X1, X2, X4))
U37_gga(X1, X2, X3, convertcA_out_gga(X1, X2, X4)) → U38_gga(X1, X2, X3, timescE_in_gga(X4, X2, X3))
U38_gga(X1, X2, X3, timescE_out_gga(X4, X2, X3)) → convertcC_out_gga(.(s(0), X1), X2, s(X3))
convertcC_in_gga(.(s(s(X1)), X2), X3, s(s(X4))) → U39_gga(X1, X2, X3, X4, convertcC_in_gga(.(X1, X2), X3, X4))
U39_gga(X1, X2, X3, X4, convertcC_out_gga(.(X1, X2), X3, X4)) → convertcC_out_gga(.(s(s(X1)), X2), X3, s(s(X4)))
U35_gga(X1, X2, X3, X4, convertcC_out_gga(.(X1, X2), X3, X5)) → U36_gga(X1, X2, X3, X4, timescE_in_gga(s(X5), X3, X4))
U36_gga(X1, X2, X3, X4, timescE_out_gga(s(X5), X3, X4)) → convertcC_out_gga(.(0, .(s(X1), X2)), X3, X4)
U28_gga(X1, X2, X3, X4, convertcC_out_gga(.(X1, X2), X3, X4)) → convertcA_out_gga(.(s(X1), X2), X3, s(X4))
U26_gga(X1, X2, X3, convertcA_out_gga(X1, X2, X4)) → U27_gga(X1, X2, X3, timescB_in_gga(X4, X2, X3))
U27_gga(X1, X2, X3, timescB_out_gga(X4, X2, X3)) → convertcA_out_gga(.(0, X1), X2, X3)
PLUSF_IN_GGA(s(X1), X2, s(X3)) → PLUSF_IN_GGA(X1, X2, X3)
PLUSF_IN_GGA(s(X1), X2) → PLUSF_IN_GGA(X1, X2)
From the DPs we obtained the following set of size-change graphs:
PLUSD_IN_GGA(s(X1), X2, s(X3)) → PLUSD_IN_GGA(X1, X2, X3)
convertcA_in_gga([], X1, 0) → convertcA_out_gga([], X1, 0)
convertcA_in_gga(.(0, X1), X2, X3) → U26_gga(X1, X2, X3, convertcA_in_gga(X1, X2, X4))
convertcA_in_gga(.(s(X1), X2), X3, s(X4)) → U28_gga(X1, X2, X3, X4, convertcC_in_gga(.(X1, X2), X3, X4))
convertcC_in_gga([], X1, 0) → convertcC_out_gga([], X1, 0)
convertcC_in_gga(.(0, []), X1, 0) → convertcC_out_gga(.(0, []), X1, 0)
convertcC_in_gga(.(0, .(0, X1)), X2, X3) → U32_gga(X1, X2, X3, convertcA_in_gga(X1, X2, X4))
U32_gga(X1, X2, X3, convertcA_out_gga(X1, X2, X4)) → U33_gga(X1, X2, X3, timescB_in_gga(X4, X2, X5))
timescB_in_gga(0, X1, 0) → timescB_out_gga(0, X1, 0)
timescB_in_gga(s(X1), X2, X3) → U29_gga(X1, X2, X3, timescB_in_gga(X1, X2, X4))
U29_gga(X1, X2, X3, timescB_out_gga(X1, X2, X4)) → U30_gga(X1, X2, X3, pluscD_in_gga(X2, X4, X3))
pluscD_in_gga(0, X1, X1) → pluscD_out_gga(0, X1, X1)
pluscD_in_gga(s(X1), X2, s(X3)) → U31_gga(X1, X2, X3, pluscD_in_gga(X1, X2, X3))
U31_gga(X1, X2, X3, pluscD_out_gga(X1, X2, X3)) → pluscD_out_gga(s(X1), X2, s(X3))
U30_gga(X1, X2, X3, pluscD_out_gga(X2, X4, X3)) → timescB_out_gga(s(X1), X2, X3)
U33_gga(X1, X2, X3, timescB_out_gga(X4, X2, X5)) → U34_gga(X1, X2, X3, timescE_in_gga(X5, X2, X3))
timescE_in_gga(0, X1, 0) → timescE_out_gga(0, X1, 0)
timescE_in_gga(s(X1), X2, X3) → U41_gga(X1, X2, X3, timescB_in_gga(X1, X2, X4))
U41_gga(X1, X2, X3, timescB_out_gga(X1, X2, X4)) → U42_gga(X1, X2, X3, pluscF_in_gga(X2, X4, X3))
pluscF_in_gga(0, X1, X1) → pluscF_out_gga(0, X1, X1)
pluscF_in_gga(s(X1), X2, s(X3)) → U40_gga(X1, X2, X3, pluscF_in_gga(X1, X2, X3))
U40_gga(X1, X2, X3, pluscF_out_gga(X1, X2, X3)) → pluscF_out_gga(s(X1), X2, s(X3))
U42_gga(X1, X2, X3, pluscF_out_gga(X2, X4, X3)) → timescE_out_gga(s(X1), X2, X3)
U34_gga(X1, X2, X3, timescE_out_gga(X5, X2, X3)) → convertcC_out_gga(.(0, .(0, X1)), X2, X3)
convertcC_in_gga(.(0, .(s(X1), X2)), X3, X4) → U35_gga(X1, X2, X3, X4, convertcC_in_gga(.(X1, X2), X3, X5))
convertcC_in_gga(.(s(0), X1), X2, s(X3)) → U37_gga(X1, X2, X3, convertcA_in_gga(X1, X2, X4))
U37_gga(X1, X2, X3, convertcA_out_gga(X1, X2, X4)) → U38_gga(X1, X2, X3, timescE_in_gga(X4, X2, X3))
U38_gga(X1, X2, X3, timescE_out_gga(X4, X2, X3)) → convertcC_out_gga(.(s(0), X1), X2, s(X3))
convertcC_in_gga(.(s(s(X1)), X2), X3, s(s(X4))) → U39_gga(X1, X2, X3, X4, convertcC_in_gga(.(X1, X2), X3, X4))
U39_gga(X1, X2, X3, X4, convertcC_out_gga(.(X1, X2), X3, X4)) → convertcC_out_gga(.(s(s(X1)), X2), X3, s(s(X4)))
U35_gga(X1, X2, X3, X4, convertcC_out_gga(.(X1, X2), X3, X5)) → U36_gga(X1, X2, X3, X4, timescE_in_gga(s(X5), X3, X4))
U36_gga(X1, X2, X3, X4, timescE_out_gga(s(X5), X3, X4)) → convertcC_out_gga(.(0, .(s(X1), X2)), X3, X4)
U28_gga(X1, X2, X3, X4, convertcC_out_gga(.(X1, X2), X3, X4)) → convertcA_out_gga(.(s(X1), X2), X3, s(X4))
U26_gga(X1, X2, X3, convertcA_out_gga(X1, X2, X4)) → U27_gga(X1, X2, X3, timescB_in_gga(X4, X2, X3))
U27_gga(X1, X2, X3, timescB_out_gga(X4, X2, X3)) → convertcA_out_gga(.(0, X1), X2, X3)
PLUSD_IN_GGA(s(X1), X2, s(X3)) → PLUSD_IN_GGA(X1, X2, X3)
PLUSD_IN_GGA(s(X1), X2) → PLUSD_IN_GGA(X1, X2)
From the DPs we obtained the following set of size-change graphs:
TIMESB_IN_GGA(s(X1), X2, X3) → TIMESB_IN_GGA(X1, X2, X4)
convertcA_in_gga([], X1, 0) → convertcA_out_gga([], X1, 0)
convertcA_in_gga(.(0, X1), X2, X3) → U26_gga(X1, X2, X3, convertcA_in_gga(X1, X2, X4))
convertcA_in_gga(.(s(X1), X2), X3, s(X4)) → U28_gga(X1, X2, X3, X4, convertcC_in_gga(.(X1, X2), X3, X4))
convertcC_in_gga([], X1, 0) → convertcC_out_gga([], X1, 0)
convertcC_in_gga(.(0, []), X1, 0) → convertcC_out_gga(.(0, []), X1, 0)
convertcC_in_gga(.(0, .(0, X1)), X2, X3) → U32_gga(X1, X2, X3, convertcA_in_gga(X1, X2, X4))
U32_gga(X1, X2, X3, convertcA_out_gga(X1, X2, X4)) → U33_gga(X1, X2, X3, timescB_in_gga(X4, X2, X5))
timescB_in_gga(0, X1, 0) → timescB_out_gga(0, X1, 0)
timescB_in_gga(s(X1), X2, X3) → U29_gga(X1, X2, X3, timescB_in_gga(X1, X2, X4))
U29_gga(X1, X2, X3, timescB_out_gga(X1, X2, X4)) → U30_gga(X1, X2, X3, pluscD_in_gga(X2, X4, X3))
pluscD_in_gga(0, X1, X1) → pluscD_out_gga(0, X1, X1)
pluscD_in_gga(s(X1), X2, s(X3)) → U31_gga(X1, X2, X3, pluscD_in_gga(X1, X2, X3))
U31_gga(X1, X2, X3, pluscD_out_gga(X1, X2, X3)) → pluscD_out_gga(s(X1), X2, s(X3))
U30_gga(X1, X2, X3, pluscD_out_gga(X2, X4, X3)) → timescB_out_gga(s(X1), X2, X3)
U33_gga(X1, X2, X3, timescB_out_gga(X4, X2, X5)) → U34_gga(X1, X2, X3, timescE_in_gga(X5, X2, X3))
timescE_in_gga(0, X1, 0) → timescE_out_gga(0, X1, 0)
timescE_in_gga(s(X1), X2, X3) → U41_gga(X1, X2, X3, timescB_in_gga(X1, X2, X4))
U41_gga(X1, X2, X3, timescB_out_gga(X1, X2, X4)) → U42_gga(X1, X2, X3, pluscF_in_gga(X2, X4, X3))
pluscF_in_gga(0, X1, X1) → pluscF_out_gga(0, X1, X1)
pluscF_in_gga(s(X1), X2, s(X3)) → U40_gga(X1, X2, X3, pluscF_in_gga(X1, X2, X3))
U40_gga(X1, X2, X3, pluscF_out_gga(X1, X2, X3)) → pluscF_out_gga(s(X1), X2, s(X3))
U42_gga(X1, X2, X3, pluscF_out_gga(X2, X4, X3)) → timescE_out_gga(s(X1), X2, X3)
U34_gga(X1, X2, X3, timescE_out_gga(X5, X2, X3)) → convertcC_out_gga(.(0, .(0, X1)), X2, X3)
convertcC_in_gga(.(0, .(s(X1), X2)), X3, X4) → U35_gga(X1, X2, X3, X4, convertcC_in_gga(.(X1, X2), X3, X5))
convertcC_in_gga(.(s(0), X1), X2, s(X3)) → U37_gga(X1, X2, X3, convertcA_in_gga(X1, X2, X4))
U37_gga(X1, X2, X3, convertcA_out_gga(X1, X2, X4)) → U38_gga(X1, X2, X3, timescE_in_gga(X4, X2, X3))
U38_gga(X1, X2, X3, timescE_out_gga(X4, X2, X3)) → convertcC_out_gga(.(s(0), X1), X2, s(X3))
convertcC_in_gga(.(s(s(X1)), X2), X3, s(s(X4))) → U39_gga(X1, X2, X3, X4, convertcC_in_gga(.(X1, X2), X3, X4))
U39_gga(X1, X2, X3, X4, convertcC_out_gga(.(X1, X2), X3, X4)) → convertcC_out_gga(.(s(s(X1)), X2), X3, s(s(X4)))
U35_gga(X1, X2, X3, X4, convertcC_out_gga(.(X1, X2), X3, X5)) → U36_gga(X1, X2, X3, X4, timescE_in_gga(s(X5), X3, X4))
U36_gga(X1, X2, X3, X4, timescE_out_gga(s(X5), X3, X4)) → convertcC_out_gga(.(0, .(s(X1), X2)), X3, X4)
U28_gga(X1, X2, X3, X4, convertcC_out_gga(.(X1, X2), X3, X4)) → convertcA_out_gga(.(s(X1), X2), X3, s(X4))
U26_gga(X1, X2, X3, convertcA_out_gga(X1, X2, X4)) → U27_gga(X1, X2, X3, timescB_in_gga(X4, X2, X3))
U27_gga(X1, X2, X3, timescB_out_gga(X4, X2, X3)) → convertcA_out_gga(.(0, X1), X2, X3)
TIMESB_IN_GGA(s(X1), X2, X3) → TIMESB_IN_GGA(X1, X2, X4)
TIMESB_IN_GGA(s(X1), X2) → TIMESB_IN_GGA(X1, X2)
From the DPs we obtained the following set of size-change graphs:
CONVERTC_IN_GGA(.(0, .(0, X1)), X2, X3) → CONVERTA_IN_GGA(X1, X2, X4)
CONVERTA_IN_GGA(.(0, X1), X2, X3) → CONVERTA_IN_GGA(X1, X2, X4)
CONVERTA_IN_GGA(.(s(X1), X2), X3, s(X4)) → CONVERTC_IN_GGA(.(X1, X2), X3, X4)
CONVERTC_IN_GGA(.(0, .(s(X1), X2)), X3, X4) → CONVERTC_IN_GGA(.(X1, X2), X3, X5)
CONVERTC_IN_GGA(.(s(0), X1), X2, s(X3)) → CONVERTA_IN_GGA(X1, X2, X4)
CONVERTC_IN_GGA(.(s(s(X1)), X2), X3, s(s(X4))) → CONVERTC_IN_GGA(.(X1, X2), X3, X4)
convertcA_in_gga([], X1, 0) → convertcA_out_gga([], X1, 0)
convertcA_in_gga(.(0, X1), X2, X3) → U26_gga(X1, X2, X3, convertcA_in_gga(X1, X2, X4))
convertcA_in_gga(.(s(X1), X2), X3, s(X4)) → U28_gga(X1, X2, X3, X4, convertcC_in_gga(.(X1, X2), X3, X4))
convertcC_in_gga([], X1, 0) → convertcC_out_gga([], X1, 0)
convertcC_in_gga(.(0, []), X1, 0) → convertcC_out_gga(.(0, []), X1, 0)
convertcC_in_gga(.(0, .(0, X1)), X2, X3) → U32_gga(X1, X2, X3, convertcA_in_gga(X1, X2, X4))
U32_gga(X1, X2, X3, convertcA_out_gga(X1, X2, X4)) → U33_gga(X1, X2, X3, timescB_in_gga(X4, X2, X5))
timescB_in_gga(0, X1, 0) → timescB_out_gga(0, X1, 0)
timescB_in_gga(s(X1), X2, X3) → U29_gga(X1, X2, X3, timescB_in_gga(X1, X2, X4))
U29_gga(X1, X2, X3, timescB_out_gga(X1, X2, X4)) → U30_gga(X1, X2, X3, pluscD_in_gga(X2, X4, X3))
pluscD_in_gga(0, X1, X1) → pluscD_out_gga(0, X1, X1)
pluscD_in_gga(s(X1), X2, s(X3)) → U31_gga(X1, X2, X3, pluscD_in_gga(X1, X2, X3))
U31_gga(X1, X2, X3, pluscD_out_gga(X1, X2, X3)) → pluscD_out_gga(s(X1), X2, s(X3))
U30_gga(X1, X2, X3, pluscD_out_gga(X2, X4, X3)) → timescB_out_gga(s(X1), X2, X3)
U33_gga(X1, X2, X3, timescB_out_gga(X4, X2, X5)) → U34_gga(X1, X2, X3, timescE_in_gga(X5, X2, X3))
timescE_in_gga(0, X1, 0) → timescE_out_gga(0, X1, 0)
timescE_in_gga(s(X1), X2, X3) → U41_gga(X1, X2, X3, timescB_in_gga(X1, X2, X4))
U41_gga(X1, X2, X3, timescB_out_gga(X1, X2, X4)) → U42_gga(X1, X2, X3, pluscF_in_gga(X2, X4, X3))
pluscF_in_gga(0, X1, X1) → pluscF_out_gga(0, X1, X1)
pluscF_in_gga(s(X1), X2, s(X3)) → U40_gga(X1, X2, X3, pluscF_in_gga(X1, X2, X3))
U40_gga(X1, X2, X3, pluscF_out_gga(X1, X2, X3)) → pluscF_out_gga(s(X1), X2, s(X3))
U42_gga(X1, X2, X3, pluscF_out_gga(X2, X4, X3)) → timescE_out_gga(s(X1), X2, X3)
U34_gga(X1, X2, X3, timescE_out_gga(X5, X2, X3)) → convertcC_out_gga(.(0, .(0, X1)), X2, X3)
convertcC_in_gga(.(0, .(s(X1), X2)), X3, X4) → U35_gga(X1, X2, X3, X4, convertcC_in_gga(.(X1, X2), X3, X5))
convertcC_in_gga(.(s(0), X1), X2, s(X3)) → U37_gga(X1, X2, X3, convertcA_in_gga(X1, X2, X4))
U37_gga(X1, X2, X3, convertcA_out_gga(X1, X2, X4)) → U38_gga(X1, X2, X3, timescE_in_gga(X4, X2, X3))
U38_gga(X1, X2, X3, timescE_out_gga(X4, X2, X3)) → convertcC_out_gga(.(s(0), X1), X2, s(X3))
convertcC_in_gga(.(s(s(X1)), X2), X3, s(s(X4))) → U39_gga(X1, X2, X3, X4, convertcC_in_gga(.(X1, X2), X3, X4))
U39_gga(X1, X2, X3, X4, convertcC_out_gga(.(X1, X2), X3, X4)) → convertcC_out_gga(.(s(s(X1)), X2), X3, s(s(X4)))
U35_gga(X1, X2, X3, X4, convertcC_out_gga(.(X1, X2), X3, X5)) → U36_gga(X1, X2, X3, X4, timescE_in_gga(s(X5), X3, X4))
U36_gga(X1, X2, X3, X4, timescE_out_gga(s(X5), X3, X4)) → convertcC_out_gga(.(0, .(s(X1), X2)), X3, X4)
U28_gga(X1, X2, X3, X4, convertcC_out_gga(.(X1, X2), X3, X4)) → convertcA_out_gga(.(s(X1), X2), X3, s(X4))
U26_gga(X1, X2, X3, convertcA_out_gga(X1, X2, X4)) → U27_gga(X1, X2, X3, timescB_in_gga(X4, X2, X3))
U27_gga(X1, X2, X3, timescB_out_gga(X4, X2, X3)) → convertcA_out_gga(.(0, X1), X2, X3)
CONVERTC_IN_GGA(.(0, .(0, X1)), X2, X3) → CONVERTA_IN_GGA(X1, X2, X4)
CONVERTA_IN_GGA(.(0, X1), X2, X3) → CONVERTA_IN_GGA(X1, X2, X4)
CONVERTA_IN_GGA(.(s(X1), X2), X3, s(X4)) → CONVERTC_IN_GGA(.(X1, X2), X3, X4)
CONVERTC_IN_GGA(.(0, .(s(X1), X2)), X3, X4) → CONVERTC_IN_GGA(.(X1, X2), X3, X5)
CONVERTC_IN_GGA(.(s(0), X1), X2, s(X3)) → CONVERTA_IN_GGA(X1, X2, X4)
CONVERTC_IN_GGA(.(s(s(X1)), X2), X3, s(s(X4))) → CONVERTC_IN_GGA(.(X1, X2), X3, X4)
CONVERTC_IN_GGA(.(0, .(0, X1)), X2) → CONVERTA_IN_GGA(X1, X2)
CONVERTA_IN_GGA(.(0, X1), X2) → CONVERTA_IN_GGA(X1, X2)
CONVERTA_IN_GGA(.(s(X1), X2), X3) → CONVERTC_IN_GGA(.(X1, X2), X3)
CONVERTC_IN_GGA(.(0, .(s(X1), X2)), X3) → CONVERTC_IN_GGA(.(X1, X2), X3)
CONVERTC_IN_GGA(.(s(0), X1), X2) → CONVERTA_IN_GGA(X1, X2)
CONVERTC_IN_GGA(.(s(s(X1)), X2), X3) → CONVERTC_IN_GGA(.(X1, X2), X3)
No rules are removed from R.
CONVERTC_IN_GGA(.(0, .(0, X1)), X2) → CONVERTA_IN_GGA(X1, X2)
CONVERTA_IN_GGA(.(0, X1), X2) → CONVERTA_IN_GGA(X1, X2)
CONVERTA_IN_GGA(.(s(X1), X2), X3) → CONVERTC_IN_GGA(.(X1, X2), X3)
CONVERTC_IN_GGA(.(0, .(s(X1), X2)), X3) → CONVERTC_IN_GGA(.(X1, X2), X3)
CONVERTC_IN_GGA(.(s(0), X1), X2) → CONVERTA_IN_GGA(X1, X2)
CONVERTC_IN_GGA(.(s(s(X1)), X2), X3) → CONVERTC_IN_GGA(.(X1, X2), X3)
POL(.(x1, x2)) = x1 + 2·x2
POL(0) = 0
POL(CONVERTA_IN_GGA(x1, x2)) = 2·x1 + x2
POL(CONVERTC_IN_GGA(x1, x2)) = x1 + x2
POL(s(x1)) = 2·x1